home *** CD-ROM | disk | FTP | other *** search
/ Amiga Plus Leser 15 / Amiga Plus Leser CD 15.iso / Tools / Development / yacas_alg / yacas_morphos / share / yacas / examples / ABIN.ys next >
Encoding:
Text File  |  2002-03-13  |  1.7 KB  |  68 lines
  1. /* Implementation of the ABIN formal grammar
  2.     (see Yacas tutorial essays) */
  3.  
  4. IsExpr(x_IsList) <-- IsBExpr(x) Or IsNExpr(x) Or IsAExpr(x);
  5.  
  6. IsProvable(x_IsList) <-- IsAxiom(x) Or IsTheorem(x);
  7.  
  8. IsAxiom(x_IsList) <-- If(IsNExpr(x) And IsBExpr(Tail(x)),
  9.  [Echo({"Axiom ", Map("ConcatStrings", x)});
  10.   True; ], False);
  11.  
  12. 10 # IsBExpr({}) <-- False;
  13.  
  14. 10 # IsBExpr({"B"}) <-- True;
  15.  
  16. 20 # IsBExpr(x_IsList) <-- x[Length(x)]="I" And
  17.  IsBExpr(Take(x, {1, Length(x)-1}));
  18.  
  19. 10 # IsNExpr({}) <-- False;
  20.  
  21. 20 # IsNExpr(x_IsList) <-- x[1] = "N" And IsExpr(Tail(x));
  22.  
  23. FindTwoExprs(x_IsList) <-- [
  24.  Local(iter, result);
  25.  For([iter:=1; result:=False;],
  26.   iter < Length(x) And Not result, iter:=iter+1 )
  27.    [
  28.     result := IsExpr(Take(x, iter))
  29.      And IsExpr(Take(x, {iter+1, Length(x)}));
  30.    ];
  31.  {result, iter-1};
  32. ];
  33.  
  34. 10 # IsAExpr(x_IsList)_(Length(x) <= 1) <-- False;
  35.  
  36. 20 # IsAExpr(x_IsList) <-- x[1] = "A" And FindTwoExprs(Tail(x))[1];
  37.  
  38. IsTheorem(x_IsList) <-- If(IsNExpr(x) And IsAExpr(Tail(x)) And
  39.   IsProvable(Concat({"N"}, Take(Tail(Tail(x)),
  40.   FindTwoExprs(Tail(Tail(x)))[2]) )),
  41.  [ Echo({"Theorem ", Map("ConcatStrings", x)[1], " derived"});
  42.   True; ], False);
  43.  
  44. AtomToCharList(x_IsAtom) <-- [
  45.   Local(index, result);
  46.   For([ index:=Length(String(x)); result:={}; ],
  47.    index > 0, index:=index-1 )
  48.    Push(result,
  49.     StringMid(index, 1, String(x)));
  50.   result;
  51. ];
  52.  
  53. ABIN(x_IsAtom) <-- If(IsProvable(AtomToCharList(x)),
  54.  True,
  55.  [Echo({x, "cannot be proved"}); False; ]);
  56.  
  57. /* Examples */
  58. IsProvable({"N", "A", "B", "I", "B", "I"});
  59. ABIN(NAAABIBBB);
  60. ABIN(NAAABNBIIABBIINB);
  61. ABIN(NAABIBIBIII);
  62. ABIN(NAABIIBIABINABIBI);
  63. ABIN(NABNANBB);
  64. ABIN(NAABIBIIBI);
  65. ABIN(NAAABBIBNB);
  66. ABIN(NAABIIBIABINABIBI);
  67. /* True but unprovable */ ABIN(NANBB);
  68.